// ***** This file is automatically generated from Numeric.java.jpp

package daikon.inv.binary.twoString;

import daikon.*;
import daikon.inv.*;
import daikon.inv.unary.sequence.*;
import daikon.inv.unary.scalar.*;
import daikon.inv.binary.twoScalar.*;
import daikon.inv.binary.twoString.*;
import daikon.derive.binary.*;
import daikon.suppress.*;
import daikon.Quantify.QuantFlags;
import static daikon.inv.Invariant.asInvClass;

import plume.*;
import java.util.*;

/**
 * Baseclass for binary numeric invariants.
 *
 * Each specific invariant is implemented in a subclass (typically, in
 * this file).  The subclass must provide the methods instantiate(),
 * check(), and format(). Symmetric functions should define
 * is_symmetric() to return true.
 **/
public abstract class StdString extends TwoString {

  // We are Serializable, so we specify a version to allow changes to
  // method signatures without breaking serialization.  If you add or
  // remove fields, you should change this number to the current date.
  static final long serialVersionUID = 20060609L;

  protected StdString(PptSlice ppt, boolean swap) {
    super(ppt);
    this.swap = swap;
  }

  protected StdString(boolean swap) {
    super();
    this.swap = swap;
  }

  /**
   * Returns true if it is ok to instantiate a numeric invariant over the
   * specified slice.
   */
  public boolean instantiate_ok (VarInfo[] vis) {

    ProglangType type1 = vis[0].file_rep_type;
    ProglangType type2 = vis[1].file_rep_type;
    if (!type1.isString() || !type2.isString()) {
      return (false);
    }

    return (true);
  }

  public boolean isExact() {
    return true;
  }

  public String repr() {
    return UtilMDE.unqualified_name (getClass()) + ": " + format() +
      (swap ? " [swapped]" : " [unswapped]");
  }

  /**
   * Returns a string in the specified format that describes the invariant.
   *
   * The generic format string is obtained from the subclass specific
   * get_format_str().  Instances of %varN% are replaced by the variable
   * name in the specified format.
   */
  public String format_using(OutputFormat format) {

    if (ppt == null)
      return (String.format ("proto ppt [class %s] format %s", getClass(),
                             get_format_str (format)));
    String fmt_str = get_format_str (format);
    String v1 = null;
    String v2 = null;

      v1 = var1().name_using(format);
      v2 = var2().name_using(format);

    // Note that we do not use String.replaceAll here, because that's
    // inseparable from the regex library, and we don't want to have to
    // escape v1 with something like
    // v1.replaceAll("([\\$\\\\])", "\\\\$1")
    fmt_str = UtilMDE.replaceString(fmt_str, "%var1%", v1);
    fmt_str = UtilMDE.replaceString(fmt_str, "%var2%", v2);

    if (false && (format == OutputFormat.DAIKON)) {
      fmt_str = "[" + getClass() + "]" + fmt_str + " ("
             + var1().get_value_info() + ", " + var2().get_value_info() +  ")";
    }
    return (fmt_str);
  }

  /**
   * Calls the function specific equal check and returns the correct
   * status.
   */

  public InvariantStatus check_modified(String x, String y, int count) {

    try {
      if (eq_check (x, y))
        return (InvariantStatus.NO_CHANGE);
      else
        return (InvariantStatus.FALSIFIED);
    } catch (Exception e) {
      return (InvariantStatus.FALSIFIED);
    }
  }

  /**
   * Checks to see if 'x[a] op y[b]' where 'x[] op y[]' and 'a == b'.
   * Doesn't catch the case where a = b+1.
   */
  public /*@Nullable*/ DiscardInfo is_subscript (VarInfo[] vis) {

    VarInfo v1 = var1(vis);
    VarInfo v2 = var2(vis);

    // Make sure each var is a sequence subscript
    if (!v1.isDerived() || !(v1.derived instanceof SequenceStringSubscript))
      return (null);
    if (!v2.isDerived() || !(v2.derived instanceof SequenceStringSubscript))
      return (null);

    SequenceStringSubscript der1 = (SequenceStringSubscript) v1.derived;
    SequenceStringSubscript der2 = (SequenceStringSubscript) v2.derived;

    // Make sure the shifts match
    if (der1.index_shift != der2.index_shift)
      return (null);

    // Look for this invariant over a sequence
    String cstr = getClass().getName();
    cstr = cstr.replaceFirst ("Numeric", "PairwiseNumeric");
    cstr = cstr.replaceFirst ("twoScalar", "twoSequence");
    cstr = cstr.replaceFirst ("twoFloat", "twoSequence");
    Class<? extends Invariant> pairwise_class;
    try {
      pairwise_class = asInvClass(Class.forName (cstr));
    } catch (Exception e) {
      throw new Error ("can't create class for " + cstr, e);
    }
    Invariant inv = find (pairwise_class, der1.seqvar(), der2.seqvar());
    if (inv == null)
      return (null);

    // Look to see if the subscripts are equal
    Invariant subinv = find (StringEqual.class, der1.sclvar(), der2.sclvar());
    if (subinv == null)
      return (null);

    return new DiscardInfo(this, DiscardCode.obvious, "Implied by " +
                           inv.format() + " and " + subinv.format());
  }

  public /*@Nullable*/ DiscardInfo isObviousDynamically (VarInfo[] vis) {

    DiscardInfo super_result = super.isObviousDynamically(vis);
    if (super_result != null)
      return super_result;

      // any relation across subscripts is made obvious by the same
      // relation across the original sequence if the subscripts are equal
      DiscardInfo result = is_subscript (vis);
      if (result != null) return result;

    // Check for invariant specific obvious checks.  The obvious_checks
    // method returns an array of arrays of antecedents.  If all of the
    // antecedents in an array are true, then the invariant is obvoius.
    InvDef[][] obvious_arr = obvious_checks (vis);
    obvious_loop:
    for (int i = 0; i < obvious_arr.length; i++) {
      InvDef[] antecedents = obvious_arr[i];
      StringBuffer why = null;
      for (int j = 0; j < antecedents.length; j++) {
        Invariant inv = antecedents[j].find ();
        if (inv == null)
          continue obvious_loop;
        if (why == null)
          why = new StringBuffer(inv.format());
        else {
          why.append(" and ");
          why.append(inv.format());
        }
      }
      return new DiscardInfo (this, DiscardCode.obvious, "Implied by " + why);
    }

    return (null);
  }

  /**
   * Return a format string for the specified output format.  Each instance
   * of %varN% will be replaced by the correct name for varN.
   */
  public abstract String get_format_str (OutputFormat format);

  /**
   * Returns true if x and y don't invalidate the invariant.
   */
  public abstract boolean eq_check (String x, String y);

  /**
   * Returns an array of arrays of antecedents.  If all of the
   * antecedents in any array are true, then the invariant is obvious.
   */
  public InvDef[][] obvious_checks (VarInfo[] vis) {
    return (new InvDef[][] {});
  }

  public static List</*@Prototype*/ Invariant> get_proto_all() {

    List</*@Prototype*/ Invariant> result = new ArrayList</*@Prototype*/ Invariant>();

        result.add (SubString.get_proto(false));
        result.add (SubString.get_proto(true));

    // System.out.printf ("%s get proto: %s\n", StdString.class, result);
    return (result);
  }

  // suppressor definitions, used by many of the classes below
  protected static NISuppressor

    var1_eq_var2    = new NISuppressor (0, 1, StringEqual.class),
    var2_eq_var1    = new NISuppressor (0, 1, StringEqual.class);

  //
  // Int and Float Numeric Invariants
  //

//
// Standard String invariants
//

  /**
   * Represents the substring invariant between
   * two String scalars.  Prints as <samp>x is a substring of y</samp>.
   */
  public static class SubString extends StdString {
    // We are Serializable, so we specify a version to allow changes to
    // method signatures without breaking serialization.  If you add or
    // remove fields, you should change this number to the current date.
    static final long serialVersionUID = 20081113L;

    protected SubString (PptSlice ppt, boolean swap) {
      super(ppt, swap);
    }

    protected SubString (boolean swap) {
      super(swap);
    }

    private static /*@Prototype*/ SubString proto = new /*@Prototype*/ SubString (false);
    private static /*@Prototype*/ SubString proto_swap = new /*@Prototype*/ SubString (true);

    public static /*@Prototype*/ SubString get_proto (boolean swap) {
      if (swap) {
        return (proto_swap);
      } else {
        return (proto);
      }
    }

    // Variables starting with dkconfig_ should only be set via the
    // daikon.config.Configuration interface.
    /** Boolean.  True iff SubString invariants should be considered. **/
    public static boolean dkconfig_enabled = false;

    /** Returns whether or not this invariant is enabled **/
    public boolean enabled() { return dkconfig_enabled; }

    protected SubString instantiate_dyn (PptSlice slice) /*@Prototype*/ {
      return new SubString (slice, swap);
    }

    public String get_format_str (OutputFormat format) {
      if (format == OutputFormat.DAIKON) {
        return "%var1% is a substring of %var2%";
      } else if (format.isJavaFamily()) {
        return "%var2%.contains(%var1%)";
      } else {
        return format_unimplemented(format);
      }
    }

    public boolean eq_check (String x, String y) {
      return (y.contains (x));
    }

    /** Justified as long as there are samples **/
    protected double computeConfidence() {
      if (ppt.num_samples() == 0) {
        return Invariant.CONFIDENCE_UNJUSTIFIED;
      }

      return Invariant.CONFIDENCE_JUSTIFIED;
    }

    /**
     * Returns a list of non-instantiating suppressions for this invariant.
     */
    public /*@NonNull*/ NISuppressionSet get_ni_suppressions() {
      if (swap) return (suppressions_swap);
      else return (suppressions);
    }

    /** definition of this invariant (the suppressee) (unswapped) **/
    private static NISuppressee suppressee
      = new NISuppressee (SubString.class, false);

    private static NISuppressionSet suppressions =
      new NISuppressionSet (new NISuppression[] {
          // v1 == v2 ==> v1 subsequence v2
          new NISuppression (var1_eq_var2, suppressee),
      });
    private static NISuppressionSet suppressions_swap = suppressions.swap();
  }

}
